package data_management;



public class User {
  
  String name;
  UserStatus status;
  
  //@ public invariant status != null;
  //@ public invariant name != null;
}

